Відмови в публікації

Колекціоную вімови і їх причини,
Можливо колись хтось захоче зайнятися теорією типів в університеті,
то хай знають шо не потрібно цього робити.

Я прийшов в математику шоб отримати всевідання в логіках
і отримати символічні передачі на всі види просторів.
В процесі цієї подорожі з повагою до вчителів минулого
Я потоваришував з найрозумнішими людьми планети і отримав бажане.
Мені не потрібна верифікація AI, я знаю шо я утримую.
То шо я утримую, утримують тільки три математичні інституції на планеті.
Ви все одно зі мною зустрінетесь коли ваші студенти наблизяться до цього в своїх сесіях з Гроком.

Ну це останній український університет куди я посилав, більше не лишилося, включаючи НАН України, їм теж не цікавий ні Лоран, ні формальні доведення. Такі справи, хлопці, можете сміливо продавати своє тіло і розум блокчейнам сім'ї Трампа і ракшасам. Якшо ви не хочете писати на Coq і Lean вас не пустять в академію. Доведеться як я тратити сотні тисяч доларів на освіту за кордоном і потім ви все одно залишитесь одні. Добре шо мені 45 і я на пенсії!

Issue XX: Аналітична Система Типів

Зауважте назву: Аналітична Система Типів. В ЛНУ навіть не розуміють чим кінцевий продукт на ринку типу Lean і Coq відрізняється від математичної моделі і екскізної архітектури. Радять мені почитати mathlib і поставити Lean. І смішно і сумно.

В додатках вони прислали дві згенеровані статті Гроком якогось дебіла, який не розуміє в чому суть статті, а просто сказав зробити прувер на Z3 і написати сттаттю, цей дебіл переслав Шаськіву відрижку грока без фільтрації, Шаськів переслав це гімно мені. Так робиться математика в Львівському Національному Університеті.

Тобто головний аргумент у відмові (аж 2 додатки і дві сесії в гроці) полягає в тому шо грок робить подібні до справжніх статті. Це кафедра логіки як так розумію чи шо.

Пане Шаськів, ви як керівник свого структурного підрозділу повинні би були прочитати Анотацію і зрозуміти шо згенеровані гроком статті не можуть бути аргументом у відмові бо є нерелевантними анотації. Може тоді вам в голову би прийшла раціональна думка не присилати мені відрижки Грока. В подальшому я буду сприймати всю кореспонденцію від ЛНУ як спам.

Цитуючи ваших дебілів: "It is unclear why reduced reliance on established libraries - such as Lean’s mathlib - should be viewed as an advantage, or why analogous analytic primitives and tactics could not be implemented within existing, more mature systems such as Lean or Rocq." Думаю шо вам ше багато десятиліть буде Unclear. Так само як дехто Unclear навіщо потрібно українська зброя, якшо є російська і американська. Навіщо нам взагалі своя наука, якшо ми можемо обслуговувати чужу науку, Horizon 2020 гранти, EuroProofNet з Dedukti без нормальних форм і канонічності, тощо. Вам не треба, то закодовуйте кон'юнктури Шольца в mathlib, успіхів в бізнесі як то кажуть! Ви не брахмани, а торгаші, ще й неосвічені до того всього.

Вступ до Маленького Ядра

Dear Dr. Сохацький Максим:

We have received the reviewer's comments on your work referenced above. In light of this report, I regret to inform you that we are unable to consider your paper for publication in our journal.

The reviewers' comments can be found at the end of this email or can be accessed by following the provided link.

We have reached a decision regarding your submission to Matematychni Studii, "Laurent: Syntentic Analysis: Laurent Schwartz: Analytical Type System for Mechanization of Theorems of Functional Analysis".

Our decision is to: Decline Submission

I hope you will not let this experience deter you from sending us your high quality work in future.

Sincerely, Oleh Skaskiv Ivan Franko National University of Lviv, Lviv [email protected]

Reviewer A:

The paper under review introduces Laurent, a new interactive proof assistant aimed at supporting formalization tasks in functional analysis. Interactive proof assistants - such as Lean and Rocq (formerly Coq) - are important tools for computer-aided discovery and formal verification of mathematical proofs. Both Lean and Rocq have been used to formalize well-known results, ranging from the classical Four Color Theorem to recent developments in condensed mathematics by Clausen and Scholze. These successes illustrate the level of maturity and robustness that contemporary state-of-the-art systems have achieved.

The author proposes Laurent as a proof assistant specifically tailored to the needs of analysis. The system is written in OCaml and integrates the Z3 SMT solver (here and below, SMT abbreviates `satisfiability modulo theories'). A link to the source code is provided, though only as a footnote on the last page, and without a clear attribution of authorship for the software.

From a technical standpoint, the system is still at an early stage. Starting Laurent via `dune exec laurent repl' launches an interactive mode that begins with a single preloaded (and trivial) goal. Although help functionality is promised, this appears not to be implemented. Only a small collection of tactics is currently supported; some of these, such as Elim and Apply, are declared but not implemented, and the paper acknowledges this.

The integration with Z3 is also limited. Nonlinear operations (multiplication, exponentiation, etc.) are not translated into SMT, effectively restricting Laurent to quantifier-free linear arithmetic. Moreover, the constructor `RealConst' discards fractional parts, so only integer constants are handled correctly at present. As a result, any statement requiring nonlinear arithmetic, transcendental functions, quantifiers, measure-theoretic constructs (including integration), or even simple fractional constants cannot be discharged automatically. While such statements may still be type-checked or proven interactively, there is currently no automation to support them.

In this light, the way Laurent is presented in the manuscript appears somewhat overly optimistic. For example, Section 3.2 introduces a syntax for Lebesgue integration, yet there is no evaluator for integrals, nor does the Z3 bridge address integration semantics.

Regarding accessibility, the paper is said to target a “formal mathematics audience.” Whatever precise meaning the author intends by this phrase, the exposition is unlikely to be accessible to readers without prior experience with proof assistants. For instance, the Backus–Naur-style grammar presented at the end of Section 1 may be too technical for an interested but inexperienced audience.

On a conceptual level, the guiding idea of creating a proof assistant “tailored to the domain-specific needs of analysis, incorporating explicit primitives for limits, measures, and algebraic structures” is debatable. It is unclear why reduced reliance on established libraries - such as Lean’s mathlib - should be viewed as an advantage, or why analogous analytic primitives and tactics could not be implemented within existing, more mature systems such as Lean or Rocq.

To illustrate this point, I experimented with a large language model by asking it to generate a simple proof assistant in OCaml using Z3 and to produce a LaTeX-formatted presentation of the system. The resulting documents (“elementary“ and “advanced“ versions) are included with this review. While not intended as a direct comparison, they raise the question of whether the current implementation and presentation of Laurent is sufficiently developed to warrant publication in a research journal.

Despite these critical remarks, my overall assessment remains cautiously positive. I appreciate the initiative to develop homegrown proof-assistant technology and agree that introducing such work to the broader mathematical community is worthwhile. As a positive example of this kind, I can mention the Lean tutorial https://leanprover-community.github.io/learn.html

I believe that an accessible introductory article on proof assistants could be valuable and appropriate for publication, provided it is genuinely written for a broad audience.

Recommendation: Decline Submission